fix(lean4/cno): finish loadStore_preserves_memory cons-case build#23
Merged
Conversation
Two root causes of the soundness-repair-in-flight build failure: 1. `private lemma` keyword was used in 3 places (L399 `setReg_cons_zero`, L404 `getReg_cons_zero`, L410 `Memory.update_same_pointwise`). The `lemma` alias is provided by Mathlib (`Mathlib.Tactic`), but this file declares no imports (`namespace CNO` at L15, no `import` lines per intentional design — L11–13 comment "No external imports required"). Lean 4 core parser only accepts `theorem`. Fixed by changing all 3 `private lemma` → `private theorem`. The L498 `setReg_cons_zero` unknown-identifier error was a downstream consequence and resolved too. 2. The nil-case `simp only []` at L482 failed with "simp made no progress" — Lean 4.16's `simp only` is strict about needing at least one lemma. After `unfold setReg getReg`, the goal reduces to `Memory.eq s.memory s.memory` by definitional equality alone (`[].get?` reduces via core `List.get?`'s `Option.none` clause, and the resulting `match none with ... | none => s` is an ι-reduction handled by the kernel). Dropping the redundant `simp only []` lets `intro a; rfl` close the goal directly. The cons-case branch (`rw [setReg_cons_zero, getReg_cons_zero]; simp only []; intro a; exact ...`) was correct once the helper lemmas above parsed. Build verified: `lake build` exits 0 across all 6 lean libraries (CNO, CNOCategory, FilesystemCNO, LambdaCNO, QuantumCNO, StatMech). Only linter warnings remain (pre-existing unused-variable noise at L37, L181; not addressed in this PR). Refs hyperpolymath/standards#133. Lean half of "[P2] absolute-zero: finish Lean CNO cons-case + Coq tier-0 rebuild". Coq tier-0 rebuild is the other half, filed separately. Co-Authored-By: Claude Opus 4.7 (1M context) <noreply@anthropic.com>
hyperpolymath
added a commit
that referenced
this pull request
May 20, 2026
Two-part deliverable under hyperpolymath/standards#133 (the absolute-zero arm of the estate proof-debt epic standards#124). **1. Rescue rebase.** The long-standing `proof-debt/standards-133-coq-rescue-wip` branch (head `1a7d7c2`, originally 4 ahead / 7 behind) rebased onto current `main`. Conflict resolution: PR #23's `loadStore_preserves_memory` cleanup (lemma → theorem; no spurious `simp only []`) preferred over the rescue branch's pre-merge form. **2. eval_deterministic discharged.** `CNO.v` previously declared `eval_deterministic` as an `Axiom` with an in-file admission that it "could be proven by induction on the evaluation relation". Now done: - New helper `Lemma step_deterministic_strong : forall s i s1 s2, step s i s1 → step s i s2 → s1 = s2` — syntactic step determinism. - `Axiom eval_deterministic` → real `Theorem eval_deterministic` (same name and type; sole in-tree caller `cno_equiv_refl` unchanged) — induction on the eval derivation, `step_deterministic_strong` forcing the intermediate state to coincide so the IH closes the tail. **Verification (build-is-oracle):** - `coqc -R common CNO common/CNO.v` exit 0 (Coq 8.18.0 + 8.20.1 — portable). - `Print Assumptions {eval_deterministic, step_deterministic_strong, cno_equiv_refl}` all "Closed under the global context". - All 11 Coq files compile clean. - `lake build` 1631/1632 green. **Docs reconciled** (`PROOF-STATUS-2026-05-18.md` + machine state under `.machine_readable/`): axiom ledger ~121 → ~120 with the discharge noted; ADR-006 (state_eq PC-exclusion) and ADR-007 (this discharge) added; STATE.a2ml session-history + components rebuilt to current truth; last-updated rolled to 2026-05-20. **Not in this PR.** ~120 other Coq `Axiom`/`Parameter` declarations across the corpus (`cno_decidable`, `eval_respects_state_eq_left`/`right`, physics/quantum model assumptions). Separate audit work. Refs hyperpolymath/standards#124 Refs hyperpolymath/standards#133 🤖 Generated with [Claude Code](https://claude.com/claude-code)
4 tasks
🔍 Hypatia Security ScanFindings: 68 issues detected
View findings[
{
"reason": "Stray AI.a2ml in root -- use 0-AI-MANIFEST.a2ml only",
"type": "banned",
"file": "AI.a2ml",
"action": "delete",
"rule_module": "root_hygiene",
"severity": "high"
},
{
"reason": "Superseded by 0-AI-MANIFEST.a2ml",
"type": "banned",
"file": "AI.djot",
"action": "delete",
"rule_module": "root_hygiene",
"severity": "high"
},
{
"reason": "No test directory or test files found",
"type": "no_tests",
"file": "/home/runner/work/absolute-zero/absolute-zero",
"action": "flag",
"rule_module": "honest_completion",
"severity": "high",
"deduction": 20
},
{
"reason": "Issue in quality.yml",
"type": "missing_workflow",
"file": "quality.yml",
"action": "create",
"rule_module": "workflow_audit",
"severity": "high"
},
{
"reason": "Issue in security-policy.yml",
"type": "missing_workflow",
"file": "security-policy.yml",
"action": "create",
"rule_module": "workflow_audit",
"severity": "medium"
},
{
"reason": "Action hyperpolymath/standards/.github/workflows/governance-reusable.yml@main needs attention",
"type": "unpinned_action",
"file": "governance.yml",
"action": "pin_sha",
"rule_module": "workflow_audit",
"severity": "high"
},
{
"reason": "Action actions/checkout@v6.0.2 needs attention",
"type": "unpinned_action",
"file": "jekyll-gh-pages.yml",
"action": "pin_sha",
"rule_module": "workflow_audit",
"severity": "medium"
},
{
"reason": "Action actions/configure-pages@v6 needs attention",
"type": "unpinned_action",
"file": "jekyll-gh-pages.yml",
"action": "pin_sha",
"rule_module": "workflow_audit",
"severity": "medium"
},
{
"reason": "Action actions/jekyll-build-pages@v1 needs attention",
"type": "unpinned_action",
"file": "jekyll-gh-pages.yml",
"action": "pin_sha",
"rule_module": "workflow_audit",
"severity": "medium"
},
{
"reason": "Action actions/upload-pages-artifact@v5 needs attention",
"type": "unpinned_action",
"file": "jekyll-gh-pages.yml",
"action": "pin_sha",
"rule_module": "workflow_audit",
"severity": "medium"
}
]Powered by Hypatia Neurosymbolic CI/CD Intelligence |
This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment
1 participant
Add this suggestion to a batch that can be applied as a single commit.This suggestion is invalid because no changes were made to the code.Suggestions cannot be applied while the pull request is closed.Suggestions cannot be applied while viewing a subset of changes.Only one suggestion per line can be applied in a batch.Add this suggestion to a batch that can be applied as a single commit.Applying suggestions on deleted lines is not supported.You must change the existing code in this line in order to create a valid suggestion.Outdated suggestions cannot be applied.This suggestion has been applied or marked resolved.Suggestions cannot be applied from pending reviews.Suggestions cannot be applied on multi-line comments.Suggestions cannot be applied while the pull request is queued to merge.Suggestion cannot be applied right now. Please check back later.
Summary
Lean half of standards#133. Repair two root-cause defects that prevented
lake buildfrom completing onproofs/lean4/CNO.lean:private lemmakeyword used in 3 helper lemmas (setReg_cons_zero,getReg_cons_zero,Memory.update_same_pointwise).lemmais a Mathlib alias, but this file ships with zero imports by intentional design (L11–13 comment). Lean 4 core parser only acceptstheorem. Switched all 3 toprivate theorem. The downstream "unknown identifiersetReg_cons_zero" error at L498 was a cascading consequence and resolved too.simp only []at L482 in the nil-branch ofloadStore_preserves_memory. Lean 4.16'ssimp onlyis strict about needing at least one lemma. Afterunfold setReg getReg, the goal reduces toMemory.eq s.memory s.memoryby definitional equality alone (kernel ι-reductions on[].get?and thematch none with ... | none => sarm). Droppingsimp only []letsintro a; rflclose.Test plan
lake build CNOexits 0lake build(full project, 6 libraries) exits 0unused variableat L37/L181/QuantumCNO; pre-existing, not in scope)sorryoraxiomintroduced inCNO.lean(verified:CNO.leanis axiom-free; the existing axioms inLambdaCNO.lean/StatMech.lean/FilesystemCNO.leanare out of scope for this issue)Refs
`Refs hyperpolymath/standards#133` — Lean half of "[P2] absolute-zero: finish Lean CNO cons-case + Coq tier-0 rebuild". The Coq tier-0 rebuild (4 axioms in `proofs/coq/common/CNO.v`: `eval_deterministic`, `cno_decidable`, `eval_respects_state_eq_{left,right}`) is the other half and will be filed separately.
🤖 Generated with Claude Code